/*
 * $Id: AnotatedProtocol.java 1259 2007-01-09 14:23:47Z tcoupaye $
 *
 * Behavior Protocols extensions for static and runtime checking
 * developed for the Julia implementation of Fractal.
 *
 * Copyright (C) 2006
 *    Formal Methods In Software Engineering Group
 *    Institute of Computer Science
 *    Academy of Sciences of the Czech Republic
 *
 * Copyright (C) 2006 France Telecom
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA
 *
 * Contact: ft@nenya.ms.mff.cuni.cz
 * Authors: Jan Kofron <kofron@nenya.ms.mff.cuni.cz>
 */

package org.objectweb.fractal.bpc.checker.utils;

import java.io.FileOutputStream;
import java.io.IOException;
import java.io.OutputStream;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.TreeSet;

/**
 * This class is used for pretty-printing of a protocol with anotated state.
 */
public class AnotatedProtocol {
    
    /**
     * Creates a new instance of AnotatedProtocol.
     * 
     * @param protocol
     *            the protocol string
     * @param indices
     *            the indices within the protocol string denotatting the state
     */
    public AnotatedProtocol(String protocol, ArrayList indices) {
        this.protocol = protocol;
        this.indices = indices;
    }
    
    /**
     * Pretty-prints the protocol and denotes the states.
     * @param file	false - print to the stdout, true - print to the file protocol.html
     */
    public void prettyPrint(boolean file) {
        try {
            if (!file)
                doPrettyPrint(System.out, "");
            else {
                FileOutputStream f = new FileOutputStream("protocol.html");
                doPrettyPrint(f, "");
                f.close();
            }
        }
        catch (IOException e) {
        	System.out.println("Error while writing protocol state");
        }
            
    }

    
    /**
     * Pretty-prints the protocol and denotes the states.
     * Prints to the given stream.
     */
    public void doPrettyPrint(OutputStream stream, String indent) throws IOException {
        TreeSet sorted = new TreeSet(indices);
        Iterator it = sorted.iterator();
        stream.write('\n');
        stream.write(new String("<html><head /><body><pre>").getBytes());
        
        int index = it.hasNext() ? ((Integer)it.next()).intValue() : -1;
        
        for (int i = 0; i < protocol.length(); ++i) {
            if (index == i) {
                
                stream.write(new String("<FONT COLOR=\"#00AA00\">").getBytes());
                stream.write(new String("&lt;HERE&gt;").getBytes());
                stream.write(new String("</FONT>").getBytes());
                
                index = it.hasNext() ? ((Integer)it.next()).intValue() : -1; 
            }
            
            char c = protocol.charAt(i);
            
            if (c == '%') {
                stream.write(new String("\n<BR><hr>\n").getBytes());
                indent = "";
            }
            else if (c == '(') {
            	stream.write('\n');
            	stream.write(indent.getBytes());
            	stream.write('(');
            	indent += INDENT;
            	//stream.write('\n');
            	//stream.write(indent.getBytes());
            }
            else if (c == ')') {
                char bc = protocol.charAt(i - 1);
                if (!((bc == '$') || (bc == '^') || (bc==']'))) {
                    stream.write('\n');
                    indent = indent.substring(0, indent.length() - INDENT.length());
                    stream.write(indent.getBytes());
                }
                else
                    indent = indent.substring(0, indent.length() - INDENT.length());
                
                stream.write(')');
                if ((protocol.length() > i + 1) && (protocol.charAt(i + 1) != '*') && (protocol.charAt(i + 1) != ';')  && (protocol.charAt(i + 1) != ')')) {
                    stream.write('\n');
                    stream.write(indent.getBytes());
                }
            }
            else if (c == '{') {
            	stream.write('\n');
            	stream.write(indent.getBytes());
            	stream.write('{');
            	indent += INDENT;
            }
            else if (c == '}') {
                stream.write('\n');
                indent = indent.substring(0, indent.length() - INDENT.length());
                stream.write(indent.getBytes());
                stream.write('}');
            	stream.write('\n');
                stream.write(indent.getBytes());
            }
            else if (c == '+') {
                stream.write('+');
                stream.write(indent.getBytes());
            }
            	
            else
                stream.write(protocol.charAt(i));
        }
        stream.write('\n');
        stream.write(new String("</pre></body></html>").getBytes());
    }
    

    /**
     * The protocol string
     */
    public String protocol;

    /**
     * The indices within the protocol string denotating the position in the
     * state space
     */
    public ArrayList indices;
    
    /**
     * How many spaces are in the indentation each step
     */
    private final static String INDENT = "   ";
}
